Nuprl Lemma : star-append_wf
11,40
postcript
pdf
T
:Type,
P
,
Q
:((
T
List)
prop{i:l}). star-append(
T
;
P
;
Q
)
(
T
List)
prop{i:l}
latex
Definitions
t
T
,
prop{i:l}
,
x
:
A
.
B
(
x
)
,
concat(
ll
)
,
append(
as
;
bs
)
,
P
Q
,
x
.
t
(
x
)
,
l_all(
L
;
T
;
x
.
P
(
x
))
,
x
:
A
.
B
(
x
)
,
star-append(
T
;
P
;
Q
)
Lemmas
l
all
wf
,
append
wf
,
concat
wf
origin
T:Type, P,Q:((T List)
prop{i:l}). star-append(T; P; Q) 
(T List)prop{i:l} T:Type, P,Q:((T List)prop{i:l}). star-append(T; P; Q) (T List)prop{i:l} Tx:A. B(x)
Q
x. t(x)
x:A. B(x)